{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, TypeOperators,
  FlexibleContexts, ScopedTypeVariables, ViewPatterns, FlexibleInstances,
  QuasiQuotes, UndecidableInstances, Rank2Types, TemplateHaskell #-}

{- |

Module      :  Data.Yoko.ReflectBase
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

The basic @yoko@ reflection concepts.

-}
module Data.Yoko.ReflectBase where

import Type.Yoko
import Data.Yoko.Generic


-- | The range of a constructor.
type family Range dc

-- | The @Tag@ of a constructor type is a type-level reflection of its
-- constructor name.
type family Tag dc

-- | The set of a types's constructor types.
data family DCs t :: * -> *

-- | The \"Datatype Constructor\" class.
class (DT (Range dc), dc ::: DCs (Range dc), Generic dc) => DC dc where
  -- | The string name of this constructor.
  occName :: [qP|dc|] -> String 
  -- | The evidence that this constructor is a member of the datatype
  -- constructor set of its range.
  tag :: DCs (Range dc) dc; tag = membership
  -- | Project this constructor from its range.
  to :: Range dc -> Maybe (RMNI dc)
  to (disband -> NP tg fds) = case eqT tg (tag :: DCs (Range dc) dc) of
    Just Refl -> Just fds
    _ -> Nothing
  -- | Embed this constructor in its range.
  fr :: RMNI dc -> Range dc

data DCSet dc where DCSet :: DC dc => DCSet dc
data DCOf t dc where DCOf :: (t ~ Range dc) => DCOf t dc





type AnRMN m u = NP u (RM m :. N)
type Disbanded m t = AnRMN m (DCs t)

disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)
disbanded = NP tag

band :: forall t. DT t => Disbanded IdM t -> t
band (NP u fds) = case weakenTo [qP|DCOf t :: * -> *|] u of
  DCOf -> case weaken u of DCSet -> fr fds




type instance s ::? DCs t = s ::? Fin (DCs t)
instance (Etinif (DCs t), s ::: Fin (DCs t)) => s ::: DCs t where
  membership = membershipFin
instance (Etinif (DCs t), SetModel (Fin (DCs t))) => SetModel (DCs t) where
  evidence u x = evidence (toFin u) x
instance (Finite (DCs t), Fin (DCs t) :=> v) => DCs t :=> v where
  weaken = weakenFin
type instance WitnessBT (DCs t) u = WitnessBTFin (DCs t) u
instance (Finite (DCs t), EqT (Fin (DCs t))) => EqT (DCs t) where
  eqT = eqTFin

-- | A type-sum of the types in this type's binding group, including
-- itself. @DTs t@ is comparable to the bingin group of @t@.
type family DTs t :: * -> *
 
-- | The "DataType" class.
class (SetModel (DTs t), EqT (DTs t),
       SetModel (DCs t), EqT (DCs t), Finite (DCs t),
       DCs t :=> DCSet, DCs t :=> DCOf t) => DT t where
  -- | The string name of this datatype's original package.
  packageName :: [qP|t|] -> String
  -- | The string name of this datatype's original module.
  moduleName :: [qP|t|] -> String
  -- | /Disband/ this type into one of its data constructors.
  disband :: t -> Disbanded IdM t





fmap concat $ mapM obvious_membership [''DCSet, ''DCOf]
instance SetModel DCSet where evidence DCSet x = x
instance SetModel (DCOf t) where evidence DCOf x = x
